smt2: flatten FPA-encoded floats to their IEEE bit pattern by tautschnig · Pull Request #9031 · diffblue/cbmc

tautschnig · 2026-06-08T10:36:00Z

smt2_convt::flatten2bv is reached when a value has to be turned into a plain bit-vector, e.g. at a union/byte-access (type-punning) boundary. For a floatbv operand encoded with the SMT-LIB FloatingPoint theory it previously asserted !use_FPA_theory and gave up, because that theory has no float-to-bit-vector operation. As a result any program that reads the raw bytes of an FPA-encoded float under an FPA solver (--cprover-smt2, or --z3/--cvc5/--bitwuzla with --fpa) hit an invariant violation -- for example reading a double's bit pattern via a union { double d; uint64_t i; }.

Two shapes cover the cases that actually arise from type-punning, and both are emitted without needing a float-to-bit-vector operation:

a constant: the IEEE interchange bit pattern is exactly the value's bit-vector representation, so it is emitted as a literal bit-vector;
a bit-pattern reinterpret (float)bits (a typecast from a same-width generic bit-vector, as produced when lowering byte operators): flattening recovers precisely those bits, i.e. the typecast operand.

A non-constant FPA float that is not such a reinterpret would require the bvfromfloat round-trip (a fresh bit-vector b with to_fp(b) = x), which has to be registered by find_symbols; that case does not arise from the byte-/union-lowering paths and is left as a clearly-reported unsupported case rather than the previous blanket invariant.

SAT mode is unaffected: use_FPA_theory is false there, so the existing convert_expr(expr) path is taken unchanged.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Copilot

Pull request overview

This PR updates smt2_convt::flatten2bv to support flattening floatbv expressions when using the SMT-LIB FloatingPoint (FPA) theory, addressing crashes when a program type-puns floats (e.g., union/byte-access to read IEEE bit patterns) under --smt2 --fpa.

Changes:

Add an FPA-specific flatten2bv path for floatbv that can emit IEEE bit-pattern bit-vectors for float constants.
Recognize and flatten the common “bit-pattern reinterpret” shape (float)bits by emitting the underlying same-width bit-vector operand.
Replace the previous blanket !use_FPA_theory invariant with a narrower “unsupported shape” failure for non-constant, non-reinterpret FPA floats.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

codecov · 2026-06-08T12:33:06Z

Codecov Report

❌ Patch coverage is 96.15385% with 1 line in your changes missing coverage. Please review.
✅ Project coverage is 80.59%. Comparing base (4ed6b6d) to head (201c968).

Files with missing lines	Patch %	Lines
src/solvers/smt2/smt2_conv.cpp	88.88%	1 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9031   +/-   ##
========================================
  Coverage    80.59%   80.59%           
========================================
  Files         1713     1713           
  Lines       189403   189427   +24     
  Branches        73       73           
========================================
+ Hits        152647   152669   +22     
- Misses       36756    36758    +2

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

kroening · 2026-06-09T18:07:03Z

Can this be generalised beyond constants by using the FPA to bit vector conversion operator?

tautschnig · 2026-06-10T04:08:46Z

Can this be generalised beyond constants by using the FPA to bit vector conversion operator?

The general case is already handled via bvfromfloat, and this current UNEXPECTEDCASE is really unreachable as every non-constant path of such a conversion will be subject to lower_byte_operators, which produces float typecasts, which in turn will be handled by bvfromfloat.

If we want to handle some future scenario where such a non-constant conversion would not be subject to lower_byte_operators this is doable, but it seems to be considerable extra work.

kroening · 2026-06-10T14:49:53Z

Ok, at the very least the description should be changed; the SMT-LIB FP theory does have a float-to-bit-vector operator, namely
((_ fp.to_ubv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))
((_ fp.to_sbv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))

kroening · 2026-06-10T14:50:13Z

And I would probably add some narrative why these aren't used.

tautschnig · 2026-06-11T08:03:05Z

And I would probably add some narrative why these aren't used.

Good point — fixed the wording. fp.to_ubv/fp.to_sbv are value conversions (round to integer; undefined on NaN/∞/out‑of‑range), not the IEEE‑754 bit‑pattern reinterpret, and SMT‑LIB has no standard inverse of (_ to_fp …). Updated the comment, commit message and test docs to say that and why those operators aren't used.

kroening · 2026-06-11T13:57:31Z

+      // from type-punning (union / byte access) without such an operator:
+      //   - a constant: the IEEE interchange bit pattern is the value's
+      //     bit-vector representation, emitted as a literal;
+      //   - a bit-pattern reinterpret `(float)bits` (a typecast from a


The narrative is still very confusing. (float)bits looks syntactically like a C type cast, which is of course a value conversion, and not a bit-pattern reinterpretation.

kroening · 2026-06-11T13:59:15Z

+        const auto &tc = to_typecast_expr(expr);
+        if(
+          tc.op().type().id() == ID_bv &&
+          boolbv_width(tc.op().type()) == boolbv_width(type))


BTW, not least owing to this confusion, I am considering to replace the double cast via bv_typet by a new operator, named say reinterpret_cast.

Isn't that where we usually use byte_extract or extractbits?

Thinking about this again the double cast quite possibly is the result of lowering a byte_extract. Let me see if we can replace that by extractbits.

Suppose you see an extracbits that extracts all bits. Wouldn't that confuse you?

Or you would expect the simplifier to remove it?

Indeed, simplify_extractbits would rewrite it straight back into a typecast. So we'd need something like a reinterpret_cast to clean this up, but actually the simpler solution is to just remove this part from the PR (as done in 201c968): just flattening float constants to their IEEE bit pattern, because this is the only branch that's truly reachable here, see also #9031 (comment).

I'll do a separate PR with a reinterpret_cast_exprt.

smt2_convt::flatten2bv is reached when a value has to be turned into a plain bit-vector, e.g. at a union/byte-access (type-punning) boundary. For a floatbv operand encoded with the SMT-LIB FloatingPoint theory it previously asserted !use_FPA_theory and gave up. As a result any program that reads the raw bytes of an FPA-encoded float constant under an FPA solver (--cprover-smt2, or --z3/--cvc5/--bitwuzla with --fpa) hit an invariant violation -- for example reading a double's bit pattern via a union { double d; uint64_t i; }. A floatbv constant's IEEE-754 interchange bit pattern is exactly its bit-vector representation (NaN payloads and signed zero included), so it is now emitted as a literal bit-vector. This is the only shape that reaches flatten2bv under FPA: a non-constant float whose bits are read is lowered by lower_byte_operators into a float typecast, which is handled by the bvfromfloat round-trip in find_symbols and never reaches flatten2bv. Any other (genuinely symbolic) float arriving here is left as a clearly-reported UNEXPECTEDCASE rather than the previous blanket invariant. SAT mode is unaffected: use_FPA_theory is false there, so the existing convert_expr(expr) path is taken unchanged. CI coverage is provided by a unit test in unit/solvers/smt2/smt2_conv.cpp that drives flatten2bv directly under solvert::CPROVER_SMT2 (use_FPA_theory == true) with an FPA-encoded `double` constant; it SIGABRTs on the previous invariant if the fix is reverted. The companion regression test under regression/cbmc/union-double-bits-fpa/ documents the user-visible union-based scenario; CPROVER's in-tree SMT2 solver does not fully support the SMT-LIB FloatingPoint theory beyond constant folding, so that test is tagged `broken-cprover-smt-backend`, but it has been manually confirmed that with the new flatten2bv emission the formula is solver-compatible under `--z3 --fpa`. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig self-assigned this Jun 8, 2026

Copilot AI review requested due to automatic review settings June 8, 2026 10:36

tautschnig requested review from TGWDB, kroening, martin-cs and peterschrammel as code owners June 8, 2026 10:36

Copilot started reviewing on behalf of tautschnig June 8, 2026 10:36 View session

Copilot AI reviewed Jun 8, 2026

View reviewed changes

Comment thread src/solvers/smt2/smt2_conv.cpp Outdated

Comment thread src/solvers/smt2/smt2_conv.cpp Outdated

tautschnig force-pushed the flatten-fpa branch from 9ab4b62 to 795c32b Compare June 8, 2026 11:35

tautschnig mentioned this pull request Jun 8, 2026

Model x86 80-bit extended long double precisely #9023

Open

5 tasks

tautschnig force-pushed the flatten-fpa branch from 795c32b to ee629cf Compare June 9, 2026 04:43

tautschnig assigned kroening and unassigned tautschnig Jun 9, 2026

kroening assigned tautschnig and unassigned kroening Jun 10, 2026

tautschnig force-pushed the flatten-fpa branch from ee629cf to fc30b0b Compare June 11, 2026 08:02

tautschnig assigned kroening and unassigned tautschnig Jun 11, 2026

kroening reviewed Jun 11, 2026

View reviewed changes

tautschnig force-pushed the flatten-fpa branch from fc30b0b to 201c968 Compare June 11, 2026 17:55

kroening approved these changes Jun 12, 2026

View reviewed changes

kroening merged commit f29a0f0 into diffblue:develop Jun 12, 2026
61 of 62 checks passed

tautschnig deleted the flatten-fpa branch June 12, 2026 18:06

Conversation

tautschnig commented Jun 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

codecov Bot commented Jun 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

kroening commented Jun 9, 2026

Uh oh!

tautschnig commented Jun 10, 2026

Uh oh!

kroening commented Jun 10, 2026

Uh oh!

kroening commented Jun 10, 2026

Uh oh!

tautschnig commented Jun 11, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

tautschnig commented Jun 8, 2026 •

edited

Loading

codecov Bot commented Jun 8, 2026 •

edited

Loading